es:ES, a:Atom1, e:E. e receives a  Prop 

latex

Definitions	ES, t  T, Atom$n, x:A. B(x), E, Type, AtomFree(T;x), val(e), valtype(e), P  Q, x:T>>a, isrcv(e), b, Prop, x:AB(x), P & Q, e receives a
Lemmas	atom-free-es-valtype, assert wf, es-isrcv wf, inheres wf, es-valtype wf, es-val wf, es-E wf, event system wf